$\forall$$E$:Type, $t$:Tree($E$). right\_child($t$) $\in$ Tree($E$)